package ch.epfl.lara.matcheck.verify.provers;

trait FormulaDecider {
	/** Initializes the formula decider, returns whether the operation was successful */
	def init: Boolean

	/** Initializes the formula decider, controlling its output streams  */
	def init(outStream: java.io.PrintStream, errStream: java.io.PrintStream): Boolean

	/** Decides whether a formula is valid or not */
	def decide(formula: String): ProverResults.ProverResult
	
	/** Decides whether a formula is valid or not, controlling the output streams */
	def decide(formula: String, outStream: java.io.PrintStream, errStream: java.io.PrintStream): ProverResults.ProverResult
}
